Left Termination proof of /tmp/tmpJdYMKF/hbal

Left Termination of the query pattern hbal_tree_in_2(g, a) w.r.t. the given Prolog program could successfully be proven:

↳ Prolog

  ↳ PrologToPiTRSProof

Clauses:

hbal_tree(zero, nil).
hbal_tree(s(zero), t(x, nil, nil)).
hbal_tree(s(s(X)), t(x, L, R)) :- ','(distr(s(X), X, DL, DR), ','(hbal_tree(DL, L), hbal_tree(DR, R))).
distr(D1, X, D1, D1).
distr(D1, D2, D1, D2).
distr(D1, D2, D2, D1).

Queries:

hbal_tree(g,a).

We use the technique of [30].Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

hbal_tree_in(s(s(X)), t(x, L, R)) → U1(X, L, R, distr_in(s(X), X, DL, DR))
distr_in(D1, D2, D2, D1) → distr_out(D1, D2, D2, D1)
distr_in(D1, D2, D1, D2) → distr_out(D1, D2, D1, D2)
distr_in(D1, X, D1, D1) → distr_out(D1, X, D1, D1)
U1(X, L, R, distr_out(s(X), X, DL, DR)) → U2(X, L, R, DL, DR, hbal_tree_in(DL, L))
hbal_tree_in(s(zero), t(x, nil, nil)) → hbal_tree_out(s(zero), t(x, nil, nil))
hbal_tree_in(zero, nil) → hbal_tree_out(zero, nil)
U2(X, L, R, DL, DR, hbal_tree_out(DL, L)) → U3(X, L, R, DL, DR, hbal_tree_in(DR, R))
U3(X, L, R, DL, DR, hbal_tree_out(DR, R)) → hbal_tree_out(s(s(X)), t(x, L, R))

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

hbal_tree_in(s(s(X)), t(x, L, R)) → U1(X, L, R, distr_in(s(X), X, DL, DR))
distr_in(D1, D2, D2, D1) → distr_out(D1, D2, D2, D1)
distr_in(D1, D2, D1, D2) → distr_out(D1, D2, D1, D2)
distr_in(D1, X, D1, D1) → distr_out(D1, X, D1, D1)
U1(X, L, R, distr_out(s(X), X, DL, DR)) → U2(X, L, R, DL, DR, hbal_tree_in(DL, L))
hbal_tree_in(s(zero), t(x, nil, nil)) → hbal_tree_out(s(zero), t(x, nil, nil))
hbal_tree_in(zero, nil) → hbal_tree_out(zero, nil)
U2(X, L, R, DL, DR, hbal_tree_out(DL, L)) → U3(X, L, R, DL, DR, hbal_tree_in(DR, R))
U3(X, L, R, DL, DR, hbal_tree_out(DR, R)) → hbal_tree_out(s(s(X)), t(x, L, R))

The argument filtering Pi contains the following mapping:
hbal_tree_in(x1, x2) = hbal_tree_in(x1)
s(x1) = s(x1)
t(x1, x2, x3) = t(x1, x2, x3)
x = x
U1(x1, x2, x3, x4) = U1(x4)
distr_in(x1, x2, x3, x4) = distr_in(x1, x2)
distr_out(x1, x2, x3, x4) = distr_out(x3, x4)
U2(x1, x2, x3, x4, x5, x6) = U2(x5, x6)
zero = zero
nil = nil
hbal_tree_out(x1, x2) = hbal_tree_out(x2)
U3(x1, x2, x3, x4, x5, x6) = U3(x2, x6)

Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

HBAL_TREE_IN(s(s(X)), t(x, L, R)) → U1¹(X, L, R, distr_in(s(X), X, DL, DR))
HBAL_TREE_IN(s(s(X)), t(x, L, R)) → DISTR_IN(s(X), X, DL, DR)
U1¹(X, L, R, distr_out(s(X), X, DL, DR)) → U2¹(X, L, R, DL, DR, hbal_tree_in(DL, L))
U1¹(X, L, R, distr_out(s(X), X, DL, DR)) → HBAL_TREE_IN(DL, L)
U2¹(X, L, R, DL, DR, hbal_tree_out(DL, L)) → U3¹(X, L, R, DL, DR, hbal_tree_in(DR, R))
U2¹(X, L, R, DL, DR, hbal_tree_out(DL, L)) → HBAL_TREE_IN(DR, R)

The TRS R consists of the following rules:

hbal_tree_in(s(s(X)), t(x, L, R)) → U1(X, L, R, distr_in(s(X), X, DL, DR))
distr_in(D1, D2, D2, D1) → distr_out(D1, D2, D2, D1)
distr_in(D1, D2, D1, D2) → distr_out(D1, D2, D1, D2)
distr_in(D1, X, D1, D1) → distr_out(D1, X, D1, D1)
U1(X, L, R, distr_out(s(X), X, DL, DR)) → U2(X, L, R, DL, DR, hbal_tree_in(DL, L))
hbal_tree_in(s(zero), t(x, nil, nil)) → hbal_tree_out(s(zero), t(x, nil, nil))
hbal_tree_in(zero, nil) → hbal_tree_out(zero, nil)
U2(X, L, R, DL, DR, hbal_tree_out(DL, L)) → U3(X, L, R, DL, DR, hbal_tree_in(DR, R))
U3(X, L, R, DL, DR, hbal_tree_out(DR, R)) → hbal_tree_out(s(s(X)), t(x, L, R))

The argument filtering Pi contains the following mapping:
hbal_tree_in(x1, x2) = hbal_tree_in(x1)
s(x1) = s(x1)
t(x1, x2, x3) = t(x1, x2, x3)
x = x
U1(x1, x2, x3, x4) = U1(x4)
distr_in(x1, x2, x3, x4) = distr_in(x1, x2)
distr_out(x1, x2, x3, x4) = distr_out(x3, x4)
U2(x1, x2, x3, x4, x5, x6) = U2(x5, x6)
zero = zero
nil = nil
hbal_tree_out(x1, x2) = hbal_tree_out(x2)
U3(x1, x2, x3, x4, x5, x6) = U3(x2, x6)
DISTR_IN(x1, x2, x3, x4) = DISTR_IN(x1, x2)
U2¹(x1, x2, x3, x4, x5, x6) = U2¹(x5, x6)
U3¹(x1, x2, x3, x4, x5, x6) = U3¹(x2, x6)
HBAL_TREE_IN(x1, x2) = HBAL_TREE_IN(x1)
U1¹(x1, x2, x3, x4) = U1¹(x4)

We have to consider all (P,R,Pi)-chains

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

HBAL_TREE_IN(s(s(X)), t(x, L, R)) → U1¹(X, L, R, distr_in(s(X), X, DL, DR))
HBAL_TREE_IN(s(s(X)), t(x, L, R)) → DISTR_IN(s(X), X, DL, DR)
U1¹(X, L, R, distr_out(s(X), X, DL, DR)) → U2¹(X, L, R, DL, DR, hbal_tree_in(DL, L))
U1¹(X, L, R, distr_out(s(X), X, DL, DR)) → HBAL_TREE_IN(DL, L)
U2¹(X, L, R, DL, DR, hbal_tree_out(DL, L)) → U3¹(X, L, R, DL, DR, hbal_tree_in(DR, R))
U2¹(X, L, R, DL, DR, hbal_tree_out(DL, L)) → HBAL_TREE_IN(DR, R)

The TRS R consists of the following rules:

hbal_tree_in(s(s(X)), t(x, L, R)) → U1(X, L, R, distr_in(s(X), X, DL, DR))
distr_in(D1, D2, D2, D1) → distr_out(D1, D2, D2, D1)
distr_in(D1, D2, D1, D2) → distr_out(D1, D2, D1, D2)
distr_in(D1, X, D1, D1) → distr_out(D1, X, D1, D1)
U1(X, L, R, distr_out(s(X), X, DL, DR)) → U2(X, L, R, DL, DR, hbal_tree_in(DL, L))
hbal_tree_in(s(zero), t(x, nil, nil)) → hbal_tree_out(s(zero), t(x, nil, nil))
hbal_tree_in(zero, nil) → hbal_tree_out(zero, nil)
U2(X, L, R, DL, DR, hbal_tree_out(DL, L)) → U3(X, L, R, DL, DR, hbal_tree_in(DR, R))
U3(X, L, R, DL, DR, hbal_tree_out(DR, R)) → hbal_tree_out(s(s(X)), t(x, L, R))

The argument filtering Pi contains the following mapping:
hbal_tree_in(x1, x2) = hbal_tree_in(x1)
s(x1) = s(x1)
t(x1, x2, x3) = t(x1, x2, x3)
x = x
U1(x1, x2, x3, x4) = U1(x4)
distr_in(x1, x2, x3, x4) = distr_in(x1, x2)
distr_out(x1, x2, x3, x4) = distr_out(x3, x4)
U2(x1, x2, x3, x4, x5, x6) = U2(x5, x6)
zero = zero
nil = nil
hbal_tree_out(x1, x2) = hbal_tree_out(x2)
U3(x1, x2, x3, x4, x5, x6) = U3(x2, x6)
DISTR_IN(x1, x2, x3, x4) = DISTR_IN(x1, x2)
U2¹(x1, x2, x3, x4, x5, x6) = U2¹(x5, x6)
U3¹(x1, x2, x3, x4, x5, x6) = U3¹(x2, x6)
HBAL_TREE_IN(x1, x2) = HBAL_TREE_IN(x1)
U1¹(x1, x2, x3, x4) = U1¹(x4)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 1 SCC with 2 less nodes.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

U1¹(X, L, R, distr_out(s(X), X, DL, DR)) → HBAL_TREE_IN(DL, L)
U2¹(X, L, R, DL, DR, hbal_tree_out(DL, L)) → HBAL_TREE_IN(DR, R)
HBAL_TREE_IN(s(s(X)), t(x, L, R)) → U1¹(X, L, R, distr_in(s(X), X, DL, DR))
U1¹(X, L, R, distr_out(s(X), X, DL, DR)) → U2¹(X, L, R, DL, DR, hbal_tree_in(DL, L))

The TRS R consists of the following rules:

hbal_tree_in(s(s(X)), t(x, L, R)) → U1(X, L, R, distr_in(s(X), X, DL, DR))
distr_in(D1, D2, D2, D1) → distr_out(D1, D2, D2, D1)
distr_in(D1, D2, D1, D2) → distr_out(D1, D2, D1, D2)
distr_in(D1, X, D1, D1) → distr_out(D1, X, D1, D1)
U1(X, L, R, distr_out(s(X), X, DL, DR)) → U2(X, L, R, DL, DR, hbal_tree_in(DL, L))
hbal_tree_in(s(zero), t(x, nil, nil)) → hbal_tree_out(s(zero), t(x, nil, nil))
hbal_tree_in(zero, nil) → hbal_tree_out(zero, nil)
U2(X, L, R, DL, DR, hbal_tree_out(DL, L)) → U3(X, L, R, DL, DR, hbal_tree_in(DR, R))
U3(X, L, R, DL, DR, hbal_tree_out(DR, R)) → hbal_tree_out(s(s(X)), t(x, L, R))

The argument filtering Pi contains the following mapping:
hbal_tree_in(x1, x2) = hbal_tree_in(x1)
s(x1) = s(x1)
t(x1, x2, x3) = t(x1, x2, x3)
x = x
U1(x1, x2, x3, x4) = U1(x4)
distr_in(x1, x2, x3, x4) = distr_in(x1, x2)
distr_out(x1, x2, x3, x4) = distr_out(x3, x4)
U2(x1, x2, x3, x4, x5, x6) = U2(x5, x6)
zero = zero
nil = nil
hbal_tree_out(x1, x2) = hbal_tree_out(x2)
U3(x1, x2, x3, x4, x5, x6) = U3(x2, x6)
U2¹(x1, x2, x3, x4, x5, x6) = U2¹(x5, x6)
HBAL_TREE_IN(x1, x2) = HBAL_TREE_IN(x1)
U1¹(x1, x2, x3, x4) = U1¹(x4)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ PiDPToQDPProof

                ↳ QDP

                  ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

U1¹(distr_out(DL, DR)) → HBAL_TREE_IN(DL)
HBAL_TREE_IN(s(s(X))) → U1¹(distr_in(s(X), X))
U2¹(DR, hbal_tree_out(L)) → HBAL_TREE_IN(DR)
U1¹(distr_out(DL, DR)) → U2¹(DR, hbal_tree_in(DL))

The TRS R consists of the following rules:

hbal_tree_in(s(s(X))) → U1(distr_in(s(X), X))
distr_in(D1, D2) → distr_out(D2, D1)
distr_in(D1, D2) → distr_out(D1, D2)
distr_in(D1, X) → distr_out(D1, D1)
U1(distr_out(DL, DR)) → U2(DR, hbal_tree_in(DL))
hbal_tree_in(s(zero)) → hbal_tree_out(t(x, nil, nil))
hbal_tree_in(zero) → hbal_tree_out(nil)
U2(DR, hbal_tree_out(L)) → U3(L, hbal_tree_in(DR))
U3(L, hbal_tree_out(R)) → hbal_tree_out(t(x, L, R))

The set Q consists of the following terms:

hbal_tree_in(x0)
distr_in(x0, x1)
U1(x0)
U2(x0, x1)
U3(x0, x1)

We have to consider all (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

U1¹(distr_out(DL, DR)) → HBAL_TREE_IN(DL)
HBAL_TREE_IN(s(s(X))) → U1¹(distr_in(s(X), X))
U1¹(distr_out(DL, DR)) → U2¹(DR, hbal_tree_in(DL))

The remaining pairs can at least be oriented weakly.

U2¹(DR, hbal_tree_out(L)) → HBAL_TREE_IN(DR)

Used ordering: Combined order from the following AFS and order.
U1¹(x1) = U1¹(x1)
distr_out(x1, x2) = distr_out(x1, x2)
HBAL_TREE_IN(x1) = HBAL_TREE_IN(x1)
s(x1) = s(x1)
distr_in(x1, x2) = distr_in(x1, x2)
U2¹(x1, x2) = U2¹(x1)
hbal_tree_out(x1) = x1
hbal_tree_in(x1) = hbal_tree_in
U3(x1, x2) = U3(x1, x2)
t(x1, x2, x3) = t(x1, x2, x3)
x = x
U1(x1) = U1
U2(x1, x2) = U2
zero = zero
nil = nil

Recursive path order with status [2].
Quasi-Precedence:

[s₁, nil] > [U1^1₁, HBAL_{TREE_IN₁}, U2^1_1]
[s₁, nil] > distr_in₂ > distr_out₂
[s₁, nil] > t₃
U1 > [hbal_{tree_in}, U3₂, U2]

Status:

hbal_{tree_in}: multiset
distr_out₂: multiset
t₃: multiset
U3₂: multiset
nil: multiset
HBAL_{TREE_IN₁}: multiset
U2: []
U2^1₁: multiset
zero: multiset
U1^1₁: multiset
distr_in₂: multiset
s₁: multiset
U1: multiset
x: multiset

The following usable rules [17] were oriented:

distr_in(D1, X) → distr_out(D1, D1)
distr_in(D1, D2) → distr_out(D1, D2)
distr_in(D1, D2) → distr_out(D2, D1)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ PiDPToQDPProof

                ↳ QDP

                  ↳ QDPOrderProof

                    ↳ QDP

                      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

U2¹(DR, hbal_tree_out(L)) → HBAL_TREE_IN(DR)

The TRS R consists of the following rules:

hbal_tree_in(s(s(X))) → U1(distr_in(s(X), X))
distr_in(D1, D2) → distr_out(D2, D1)
distr_in(D1, D2) → distr_out(D1, D2)
distr_in(D1, X) → distr_out(D1, D1)
U1(distr_out(DL, DR)) → U2(DR, hbal_tree_in(DL))
hbal_tree_in(s(zero)) → hbal_tree_out(t(x, nil, nil))
hbal_tree_in(zero) → hbal_tree_out(nil)
U2(DR, hbal_tree_out(L)) → U3(L, hbal_tree_in(DR))
U3(L, hbal_tree_out(R)) → hbal_tree_out(t(x, L, R))

The set Q consists of the following terms:

hbal_tree_in(x0)
distr_in(x0, x1)
U1(x0)
U2(x0, x1)
U3(x0, x1)

We have to consider all (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 1 less node.